Z3 JavaScript
The Z3 distribution comes with TypeScript (and therefore JavaScript) bindings for Z3. In the following we give a few examples of using Z3 through these bindings. You can run and modify the examples locally in your browser.
The bindings do not support all features of z3. For example, you cannot (yet) create array expressions in the same way that you can create arithmetic expressions. The JavaScript bindings have the distinct advantage that they let you use z3 directly in your browser with minimal extra dependencies.
Warmup
We use a collection of basic examples to illustrate the bindings. The first example is a formula that establishes that there is no number both above 9 and below 10:
We note that the JavaScript bindings wrap z3 expressions into JavaScript options that support methods for building new expressions.
For example, the method ge is available on an arithmetic expression a. It takes one argument b and returns
and expression corresponding to the predicate a >= b.
The Z3.solve method takes a sequence of predicates and checks if there is a solution. If there is a solution, it returns a model.
Propositional Logic
Prove De Morgan's Law
What not to wear? It is well-known that developers of SAT solvers have difficulties looking sharp. They like to wear some combination of shirt and tie, but can't wear both. What should a SAT solver developer wear?
Integer Arithmetic
solve x > 2 and y < 10 and x + 2y = 7
Dogs, cats and mice
Given 100 dollars, the puzzle asks if it is possible to buy 100 animals based on their prices that are 15, 1, and 0.25 dollars, respectively.
Arrays
Arrays use the methods select and store to access and update elements. Note that
arrays are static and these operations return new arrays.
Prove Store(arr, idx, val)[idx] == val
Find unequal arrays with the same sum
We illustrate how to use the solver in finding assignments of array values that satisfy a given predicate. In this example, we want to find two arrays of length 4 that have the same sum, but are not equal:
Uninterpreted Functions
The method call is used to build expressions by applying the function node to arguments.
Prove x = y implies g(x) = g(y)
Disprove x = y implies g(g(x)) = g(y)
we illustrate the use of the Solver object in the following example. Instead of calling Z3.solve
we here create a solver object and add assertions to it. The solver.check() method is used to check
satisfiability (we expect the result to be sat for this example). The method solver.model() is used to retrieve a model:
Prove x = y implies g(x) = g(y)
Disprove that x = y implies g(g(x)) = g(y)
Solve sudoku
The popular Sudoku can be solved.
The encoding used in the following example uses arithmetic. It works here, but is not the only possible encoding approach. You can also use bit-vectors for the cells. It is generally better to use bit-vectors for finite domain problems in z3.
Arithmetic over Reals
You can create constants ranging over reals from strings that use fractions, decimal notation and from floating point numbers.
Z3 uses arbitrary precision arithmetic, so decimal positions are not truncated when you use strings to represent real numerals.
Non-linear arithmetic
Z3 uses a decision procedure for non-linear arithmetic over reals. It is based on Cylindric Algebraic Decomposition. Solutions to non-linear arithmetic formulas are no longer necessarily rational. They are represented as algebraic numbers in general and can be displayed with any number of decimal position precision.
Bit-vectors
Unlike in programming languages, there is no distinction between signed and unsigned bit-vectors. Instead the API supports operations that have different meaning depending on whether a bit-vector is treated as a signed or unsigned numeral. These are signed comparison and signed division, remainder operations.
In the following we illustrate the use of signed and unsigned less-than-or-equal:
It is easy to write formulas that mix bit-wise and arithmetic operations over bit-vectors.
Using Z3 objects wrapped in JavaScript
The following example illustrates the use of AstVector: